A, B:Type, f0:A, g0:B, F:(ABA), G:(ABB).
f:A
g:B
(f(0) = f0
& g(0) = g0
& (s:. f(s) = F(s - 1,f(s - 1),g(s - 1)) & g(s) = G(s - 1,f(s - 1),g(s - 1)))) 

latex

Definitions	f(a), x:A  B(x), t  T, x:AB(x), P  Q, x:A. B(x), s = t, False, A, , {x:A| B(x)} , , b, , P & Q, P  Q, Unit, left + right, x:A. B(x), , Type, x(s1,s2,s3), <a, b>, let x,y = A in B(x;y), x.A(x), primrec(n;b;c), t.2, t.1
Lemmas	eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int